preinit1R{$x:ut2, $a:ut2}
preinit1R(i; X; p; x0; P)
== ([Rpre(i;"$x" : X;"$a";p;s.P(s."$x")); Rinit(i;X;"$x";inl x0 )]) 

latex

---

clarification:

preinit1R{$x:ut2, $a:ut2}
preinit1R(i; X; p; x0; P)
== ([Rpre(i;"$x" : X;"$a";p;s.P(s."$x")) / [Rinit(i;X;"$x";inl x0 ) / []]]) 

latex

Definitions

(L), Rpre(loc;ds;a;p;P), x : v, x.A(x), f(a), s.x, [car / cdr], Rinit(loc;T;x;v), "$x", inl x , []